Nuprl Lemma : mul_nzero
11,40
postcript
pdf
a
,
b
:int_nzero. nequal(
; (
a
*
b
); 0)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
int_nzero
Lemmas
int
nzero
wf
,
mul
wf
nzero
origin
a,b:int_nzero. nequal(
; (a * b); 0) a,b:int_nzero. nequal(; (a * b); 0) 
Tx:A. B(x)